ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da), es:ES, i:Id.
(x:Id. vartype(i;x)  ds(x)?Top)
 (e:E. loc(e) = i  valtype(e)  Valtype(da;kind(e)))
 (n:, e1, e2:{e:E| loc(e) = i }. Dec(ecl-es-halt(es;x)(n,e1,e2))) 

latex

Definitions

x:A. B(x), P  Q, t  T, x. t(x), P  Q, P & Q, P  Q, Prop, x:A. B(x), A, l1 || l2, P  Q, {i..j}, i  j < k, False, {i...j}, Top, S  T, AB, SQType(T), {T}, ecl-trans-halt2(ds;da;A), Valtype(da;k), x(s), , Dec(P)

Lemmas

decidable functionality, ecl-es-halt wf, ecl-halt wf, es-hist wf, ecl-es-halt-ecl-halt, event-info wf, ecl-trans-property, es-E wf, Id wf, es-loc wf, nat wf, es-valtype wf, ma-valtype wf, es-kind wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, event system wf, ecl wf, fpf wf, Knd wf, int seg wf, length wf1, ecl-trans-halt2 wf, ecl-trans wf, not wf, firstn wf, iseg weakening, iseg wf, ecl-halt-unique, iseg transitivity, firstn is iseg, le wf, length firstn, firstn firstn, decidable int equal, firstn length, decidable and, decidable assert, ecl-trans-h wf, ecl-trans-state wf, decidable all int seg, decidable not